Example 26 in [Lucas - TR'03]

Summary: Ex26_Luc03b

• CS-TRS format
• OBJ format
• Negative results:
• Positive results:
  1. Lucas' transformation (Polynomials @ MuTerm)
  2. Giesl and Middeldorp's transformation (DP + Polynomials @ MuTerm)
  3. Polynomial interpretation (MuTerm)
  4. CSRPO
  5. CSDP

CS-TRS Ex26_Luc03b (file Ex26_Luc03b.csr)

Functions:  terms cons recip sqr s 0 add dbl first nil

Constructors:  cons recip s 0 nil

Variables:  N X Y Z

Arities: 

ar(terms) = 1
ar(cons) = 2
ar(recip) = 1
ar(sqr) = 1
ar(s) = 1
ar(0) = 0
ar(add) = 2
ar(dbl) = 1
ar(first) = 2
ar(nil) = 0

Replacement map: 

µ(terms)={1}
µ(cons)={1}
µ(recip)={1}
µ(sqr)={1}
µ(s)={}
µ(0)={}
µ(add)={1,2}
µ(dbl)={1}
µ(first)={1,2}
µ(nil)={}

Rules: (file Ex26_Luc03b)  

terms(N) -> cons(recip(sqr(N)),terms(s(N)))
sqr(0) -> 0
sqr(s(X)) -> s(add(sqr(X),dbl(X)))
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
add(0,X) -> X
add(s(X),Y) -> s(add(X,Y))
first(0,X) -> nil
first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))

The CS-TRS in OBJ format (file Ex26_Luc03b.obj):

obj Ex26_Luc03b is
  sort S .
  op terms : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op recip : S -> S .
  op sqr : S -> S .
  op s : S -> S [strat (0)] .
  op 0 : -> S .
  op add : S S -> S .
  op dbl : S -> S .
  op first : S S -> S .
  op nil : -> S .
  vars N X Y Z : S .
  eq terms(N) = cons(recip(sqr(N)),terms(s(N))) .
  eq sqr(0) = 0 .
  eq sqr(s(X)) = s(add(sqr(X),dbl(X))) .
  eq dbl(0) = 0 .
  eq dbl(s(X)) = s(s(dbl(X))) .
  eq add(0,X) = X .
  eq add(s(X),Y) = s(add(X,Y)) .
  eq first(0,X) = nil .
  eq first(s(X),cons(Y,Z)) = cons(Y,first(X,Z)) .
endo

Negative results

Positive results

1. Ex26_Luc03b is proved µ-terminating in [Luc03b, Example 26] by using Lucas' transformation. The TRS Ex2_Luc03b_L:

      terms(N) -> cons(recip(sqr(N)))
      sqr(0) -> 0
      sqr(s) -> s
      dbl(0) -> 0
      dbl(s) -> s
      add(0,X) -> X
      add(s,Y) -> s
      first(0,X) -> nil
      first(s,cons(Y)) -> cons(Y)
       

   is terminating (use MuTerm).
2. The µ-termination of Ex26_Luc03b can also be proved by using Giesl and Middeldorp's tranformation: the TRS Ex26_Luc03b_GM

      a__terms(N) -> cons(recip(a__sqr(mark(N))),terms(s(N)))
      a__sqr(0) -> 0
      a__sqr(s(X)) -> s(add(sqr(X),dbl(X)))
      a__dbl(0) -> 0
      a__dbl(s(X)) -> s(s(dbl(X)))
      a__add(0,X) -> mark(X)
      a__add(s(X),Y) -> s(add(X,Y))
      a__first(0,X) -> nil
      a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z))
      mark(terms(X)) -> a__terms(mark(X))
      mark(sqr(X)) -> a__sqr(mark(X))
      mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
      mark(dbl(X)) -> a__dbl(mark(X))
      mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
      mark(cons(X1,X2)) -> cons(mark(X1),X2)
      mark(recip(X)) -> recip(mark(X))
      mark(s(X)) -> s(X)
      mark(0) -> 0
      mark(nil) -> nil
      a__terms(X) -> terms(X)
      a__sqr(X) -> sqr(X)
      a__add(X1,X2) -> add(X1,X2)
      a__dbl(X) -> dbl(X)
      a__first(X1,X2) -> first(X1,X2)
       

   is terminating (use MuTerm).
3. The µ-termination of Ex26_Luc03b can also be proved by using a polynomial interpretation (computed with MuTerm).

      [terms](X) = X + 3
      [cons](X1,X2) = X1 + 1
      [recip](X) = X
      [sqr](X) = X + 1
      [s](X) = 0
      [0] = 1
      [add](X1,X2) = X1 + X2 + 1
      [dbl](X) = X + 1
      [first](X1,X2) = X1 + 2.X2
      [nil] = 0
       

4. The µ-termination of Ex26_Luc03b can be proved by using CSRPO (proof due to Albert Rubio). Automatically can be proved by MuTerm :
   • marking map:

        m(cons,2)= {terms}
            

   • precedence:

        terms > cons, recip, sqr, terms', s
        sqr > s, add, dbl
        dbl > s
        add > s
        first > nil, cons, terms
            

   • status:

        st(first) = lex
            

5. The µ-termination of Ex26_Luc03b can be proved by using CSDP (computed by MuTerm).